1. Field of the Invention
This invention relates to structural isomorphism detection, and particularly to structural isomorphism detection involving static rewriting to provide enhanced trace equivalence identification.
2. Description of Background
Structural isomorphism refers to the existence of a 1:1 topological mapping between equal-functioned gates of a netlist. Structural isomorphism detection has numerous applications. For example, if two or more properties under verification are determined to have isomorphic logic cones driving them, one may merely verify one of the properties, and map the corresponding verification results to the other property. As another example, one may exploit the existence of structural isomorphism between gates of a netlist to infer optimal Binary Decision Diagram (BDD) orders.
The primary goal of structural isomorphism detection is to quickly identify trace-equivalent gates, i.e., gates g1 and g2, such that for any legal trace (sequence of valuations over time) over g1, there exists a legal trace with an identical sequence of valuations for g2 and vice-versa. Exact methods for identifying trace equivalence via semantic analysis require exponential resources. Structural isomorphism often requires substantially lesser resources. Unfortunately, structural isomorphism is a weak approach for identifying trace equivalence. In other words, two gates g1 and g2 may be trace equivalent, but may not have isomorphic logic cones. Thus, structural isomorphism detection fails to identify that trace equivalence.
It is well known that logic rewriting algorithms may put a netlist into a more canonical form, i.e., such that it is more likely that two gates with equivalent functions attain equivalent structures. However, existing rewriting algorithms are lossy, and thus fail to render all trace equivalent gates as having isomorphic structures. It is desired to provide a set of improved algorithms for allowing structural isomorphism detection to identify trace equivalent gates.